\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), $e$:es{-}E(${\it es}$).
\\[0ex]fischer\=\{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2\}\+
\\[0ex](${\it es}$; $L$)
\-\\[0ex]$\Rightarrow$ f{-}newround\=\{x:ut2, free:ut2, mine:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\Rightarrow$ ($\exists$\=$m$:es{-}E(${\it es}$)\+
\\[0ex](f{-}event\=\{x:ut2\}\+
\\[0ex](${\it es}$; $L$; $m$)
\-\\[0ex]$\wedge$ (\=f{-}rank\=\{i:l\}\+\+
\\[0ex](mkid\{x:ut2\}; mkid\{free:ut2\}; ${\it es}$; $e$)
\-\\[0ex]=
\\[0ex]inc{-}fst(f{-}rank\{i:l\}(mkid\{x:ut2\}; mkid\{free:ut2\}; ${\it es}$; $m$))
\\[0ex]$\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$))
\-\\[0ex]$\wedge$ es{-}locl(${\it es}$; $m$; $e$)
\\[0ex]$\wedge$ @$m$(mkid\{x:ut2\}$\rightarrow$mkid\{mine:ut2\})
\\[0ex]$\wedge$ $\forall$${\it e''}$$\in$[$m$,$e$).es{-}after(${\it es}$; mkid\{x:ut2\}; ${\it e''}$) = mkid\{mine:ut2\} $\in$ Id))
\-
\end{tabbing}